es:ES, A:Type, i:Id, ds:x:Id fp Type, conds1, conds2:k:Knd fp V:Type  (State(ds)V(A + Top)).
es-triggers-params-consistent(es;A;i;ds;conds1)
 es-triggers-params-consistent(es;A;i;ds;conds2)
 conds1 || conds2
 es-triggers-params-consistent(es;A;i;ds;conds1  conds2) 

latex

Definitions	x:A. B(x), P  Q, es-triggers-params-consistent(es;A;i;ds;conds), P & Q, x:A. B(x), t  T, , x. t(x), Top, if b then t else f fi , tt, ff, P  Q, x(s), P  Q, A, False, , Unit,
Lemmas	assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-join wf, top wf, fpf-trivial-subtype-top, decl-state wf, es-kind wf, Id wf, es-loc wf, es-E wf, fpf-compatible wf, hasloc wf, es-valtype wf, pi1 wf, fpf-ap wf, es-state wf, fpf wf, event system wf, fpf-join-dom2, fpf-join-ap-sq, bool wf, bnot wf, not wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, exists functionality wrt iff